-
Notifications
You must be signed in to change notification settings - Fork 1.1k
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
SIP-56: Better foundations for match types #18262
SIP-56: Better foundations for match types #18262
Conversation
8c754e6
to
f0339b3
Compare
c88d23a
to
aea28b9
Compare
aea28b9
to
fa9f3ad
Compare
fa9f3ad
to
f45738c
Compare
@sjrd Can you please take a look at this example that yields a recursion limit error (this doesn't work also on the current match type system)? type TupleOfRecur[T, UB, Orig] = T match
case EmptyTuple => Orig
case UB *: xs => TupleOfRecur[xs, UB, Orig]
case _ => Nothing
type TupleOf[T, UB] = TupleOfRecur[T, UB, T]
def tupleOfInt[T, Check >: T <: TupleOf[T, Int]](t: T): T = t
val ok = tupleOfInt((1, 2, 3)) //should compile
val err = tupleOfInt((1, 2, "three")) //should fail compilation This was an attempt of mine to make an upper bound check for tuple contents. sealed trait TupleCheck
type TupleOfRecur[T, UB, Orig] = T match
case EmptyTuple => TupleCheck
case UB *: xs => TupleOfRecur[xs, UB, Orig]
case _ => Nothing
type TupleOf[T, UB] = TupleOfRecur[T, UB, T]
def foo[T, __ >: TupleCheck <: TupleOf[T, Int]](t: T): T = t
val ok = foo((1, 2, 3)) //compiles
val err = foo((1, 2, "three")) //error: Type argument TupleCheck does not conform to upper bound TupleOf[(Int, Int, String), Int] |
That still doesn't work. But I think it is legit that it does not. The recursion includes trying prove This is a legit cyclic reference to me. Even as a human I don't see how to cut the recursion short. We have to attempt to prove disjointness. |
90dce88
to
a7d3e79
Compare
a9696ac
to
e248076
Compare
This is now ready for review. 🎉 The SIP was approved for the design stage, and I rebased and cleaned up everything. @WojciechMazur Could you please run an Open Community Build based on this PR? |
There seems to be plenty of new comilation errors in community build when compared with the last nightly version - 3.4.0-RC1-bin-20231123-00e9e6b-NIGHTLY:
Some of failures I've checked might be expected, eg. in
I'm not sure about some of the failures related to usage of #Edit #Edit 2 |
fa6c198
to
a089833
Compare
For now, we only have `SubTypeTest` and `LegacyPatMat`. * `SubTypeTest` is used when there is no type capture. * `LegacyPatMat` is used when there are captures. In the match type reduction algorithm, we already have a simpler path for `SubTypeTest`. The `LegacyPatMat` path is basically the same as before, but with static knowledge that we have an `HKTypeLambda`.
This is the first step in using the new specified algorithm for match type reduction. When the pattern of a case satisfies elibility conditions, we use the new algorithm. Otherwise, we fall back on the legacy algorithm. To be eligible, a pattern with at least one capture must be: an applied *class* type constructor whose arguments are all: - either a type capture, - or a fully defined type that contains no inner capture, - or the argument must be in covariant position and recursively qualify to the elibility conditions. With those criteria, all the type captures can be *computed* using `baseType`, instead of inferred through the full `TypeComparer` machinery. The new algorithm directly handles preventing widening abstract types, when doing so leads to captures being under-defined. With the legacy algorithm, this prevention is scattered elsewhere in the type comparer. Making it centralized improves the error messages in those situations; it seems they were previously entirely misleading (see changed check files).
So that they do not fall into the legacy fallback.
An abstract tycon can be matched if it is exactly equal to the scrutinee's tycon.
The error can be silenced with `-source:3.3`. In that case, illegal match types are reduced using the legacy matching algorithm, as before.
Previously the disjointnessBoundary of HKTypeLambda's was implicitly their `resultType`, through the use of `superTypeNormalized`. This was fine as long as both sides of `provablyDisjoint` ended up being HKTypeLambda's at the same time, but this may not always be the case (notably with any-kinded types). It is safer to consider type lambdas as boundaries themselves, and explicitly recurse on the result types when arities match. This change surfaced a weird case in `TypeTestsCasts`, which called `provablyDisjoint` with ill-kinded types. We now explicitly apply what I suspect are partially-erased types to wildcards to recover appropriate kinds.
… instead. Fundamentally, the `provablyEmpty(scrut)` test was meant to prevent situations where both `scrut <: pattern` and `provablyDisjoint(scrut, pattern)` are true. That is a problem because it allows a match type to reduce in two different ways depending on the context. Instead, we basically use that combination of `scrut <: pattern` and `provablydisjoint(scrut, pattern)` as the *definition* for `provablyEmpty`. When both those conditions arise together, we refuse to reduce the match type. This allows one example to pass that did not pass before, but that particular example does not seem to cause unsoundness. In a sense, `provablyEmpty` was too strong here.
Closes scala#17121. Closes scala#17944. Closes scala#18488.
This should improve consistency with the actual earlier compilers, since it means the matching algorithm will be intact. Note that the new behavior of `provablyDisjoint` is always applied, even under `-source:3.3`. This includes using `provablyDisjoint` instead of `provablyEmpty`. So it is still possible that something behaves differently than the actual earlier compilers.
This was already done for `TypeApply` in cecfb61. We apply the same logic for `Apply` nodes.
And add an additional test for another cause of infinite recursion that was fixed earlier.
This additional test demonstrates that relaxing the `isConcrete` in a particular way around `AndType`s would also cause unsoundness. This justifies new failures in the Open Community Build.
a089833
to
c3b9d9b
Compare
Type matches become more strict following scala/scala3#18262
tp.derivedAppliedType( | ||
tycon, | ||
targs.mapConserve(_.stripAnnots(keep = _.symbol.derivesFrom(defn.RefiningAnnotationClass))) | ||
) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
@sjrd Is it supposed to be possible for the targs
to be LazyRef
s? If they are, the pending
set would also fail since LazyRef
s compare using reference equality. We could call stripLazyRef
here.
I have LazyRef
s showing up in a modified version of the compiler in an example with F-bounds, but I don't have a self-contained test case that would make them show up in the unmodified compiler. If it is indeed possible for them to show up, would you have any hints on constructing a test case? In general I have difficulty constructing test cases that even trigger provablyDisjoint
to be called on a desired pair of types.
https://stackoverflow.com/q/68877939/21927647 Answer to the question: > You were not doing anything wrong, this was an implementation limitation. > > Your example compiles successfully since Scala 3.4, thanks to the changes introduced in SIP-56 "Proper specification for match types" ([text](https://docs.scala-lang.org/sips/match-types-spec.html#:~:text=This%20SIP%20proposes%20a%20proper,the%20specification%20of%20the%20language.), [PR](#18262)).
Implementation of SIP-56: Proper Specification for Match Types.